$\forall$$A$:Type, $I$:MaInterface($A$), $i$:Id. \\[0ex]($i$ $\in$ ma{-}interface{-}locs($I$)) $\Rightarrow$ ($\forall$$k$:Knd. ($k$ $\in$ ma{-}interface{-}dom($I$;$i$)) $\Rightarrow$ ($\uparrow$hasloc($k$;$i$)))